Inference at * 
Iof proof for Lemma null-ite:


  b:, x, y:Top. null(if b then x else y fi ) ~ if b then null(x) else null(y) fi  

latex

 by UnivCD THENA Auto 
THEN SplitOnConclITE THEN Auto 

latex

TH.

Definitions	Top, Unit, P  Q, P & Q, P  Q, , , b, A, b, x:A. B(x), t  T
Lemmas	top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf